a, b:. Dec(a = b) 

latex

Up	bool 1, bool 1
Definitions	t  T, x:A. B(x), Dec(P), , P  Q, P  Q, A, Unit, , False, ff, tt,
Lemmas	bool wf, not wf, btrue wf, bfalse wf, btrue neq bfalse